0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 16 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 1918 ms)
↳12 BOUNDS(1, n^2)
qs(x', Cons(x, xs)) → app(Cons(x, Nil), Cons(x', quicksort(xs)))
quicksort(Cons(x, Cons(x', xs))) → qs(x, part(x, Cons(x', xs), Nil, Nil))
quicksort(Cons(x, Nil)) → Cons(x, Nil)
quicksort(Nil) → Nil
part(x', Cons(x, xs), xs1, xs2) → part[Ite](>(x', x), x', Cons(x, xs), xs1, xs2)
part(x, Nil, xs1, xs2) → app(xs1, xs2)
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
app(Nil, ys) → ys
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
>(S(x), S(y)) → >(x, y)
>(0, y) → False
>(S(x), 0) → True
part[Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, Cons(x, xs1), xs2)
part[False][Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, Cons(x, xs2))
part[Ite](False, x', Cons(x, xs), xs1, xs2) → part[False][Ite](<(x', x), x', Cons(x, xs), xs1, xs2)
part[False][Ite](False, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, xs2)
qs(x', Cons(x, xs)) → app(Cons(x, Nil), Cons(x', quicksort(xs))) [1]
quicksort(Cons(x, Cons(x', xs))) → qs(x, part(x, Cons(x', xs), Nil, Nil)) [1]
quicksort(Cons(x, Nil)) → Cons(x, Nil) [1]
quicksort(Nil) → Nil [1]
part(x', Cons(x, xs), xs1, xs2) → part[Ite](>(x', x), x', Cons(x, xs), xs1, xs2) [1]
part(x, Nil, xs1, xs2) → app(xs1, xs2) [1]
app(Cons(x, xs), ys) → Cons(x, app(xs, ys)) [1]
app(Nil, ys) → ys [1]
notEmpty(Cons(x, xs)) → True [1]
notEmpty(Nil) → False [1]
<(S(x), S(y)) → <(x, y) [0]
<(0, S(y)) → True [0]
<(x, 0) → False [0]
>(S(x), S(y)) → >(x, y) [0]
>(0, y) → False [0]
>(S(x), 0) → True [0]
part[Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, Cons(x, xs1), xs2) [0]
part[False][Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, Cons(x, xs2)) [0]
part[Ite](False, x', Cons(x, xs), xs1, xs2) → part[False][Ite](<(x', x), x', Cons(x, xs), xs1, xs2) [0]
part[False][Ite](False, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, xs2) [0]
| > => gr |
| < => lt |
qs(x', Cons(x, xs)) → app(Cons(x, Nil), Cons(x', quicksort(xs))) [1]
quicksort(Cons(x, Cons(x', xs))) → qs(x, part(x, Cons(x', xs), Nil, Nil)) [1]
quicksort(Cons(x, Nil)) → Cons(x, Nil) [1]
quicksort(Nil) → Nil [1]
part(x', Cons(x, xs), xs1, xs2) → part[Ite](gr(x', x), x', Cons(x, xs), xs1, xs2) [1]
part(x, Nil, xs1, xs2) → app(xs1, xs2) [1]
app(Cons(x, xs), ys) → Cons(x, app(xs, ys)) [1]
app(Nil, ys) → ys [1]
notEmpty(Cons(x, xs)) → True [1]
notEmpty(Nil) → False [1]
lt(S(x), S(y)) → lt(x, y) [0]
lt(0, S(y)) → True [0]
lt(x, 0) → False [0]
gr(S(x), S(y)) → gr(x, y) [0]
gr(0, y) → False [0]
gr(S(x), 0) → True [0]
part[Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, Cons(x, xs1), xs2) [0]
part[False][Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, Cons(x, xs2)) [0]
part[Ite](False, x', Cons(x, xs), xs1, xs2) → part[False][Ite](lt(x', x), x', Cons(x, xs), xs1, xs2) [0]
part[False][Ite](False, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, xs2) [0]
qs(x', Cons(x, xs)) → app(Cons(x, Nil), Cons(x', quicksort(xs))) [1]
quicksort(Cons(x, Cons(x', xs))) → qs(x, part(x, Cons(x', xs), Nil, Nil)) [1]
quicksort(Cons(x, Nil)) → Cons(x, Nil) [1]
quicksort(Nil) → Nil [1]
part(x', Cons(x, xs), xs1, xs2) → part[Ite](gr(x', x), x', Cons(x, xs), xs1, xs2) [1]
part(x, Nil, xs1, xs2) → app(xs1, xs2) [1]
app(Cons(x, xs), ys) → Cons(x, app(xs, ys)) [1]
app(Nil, ys) → ys [1]
notEmpty(Cons(x, xs)) → True [1]
notEmpty(Nil) → False [1]
lt(S(x), S(y)) → lt(x, y) [0]
lt(0, S(y)) → True [0]
lt(x, 0) → False [0]
gr(S(x), S(y)) → gr(x, y) [0]
gr(0, y) → False [0]
gr(S(x), 0) → True [0]
part[Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, Cons(x, xs1), xs2) [0]
part[False][Ite](True, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, Cons(x, xs2)) [0]
part[Ite](False, x', Cons(x, xs), xs1, xs2) → part[False][Ite](lt(x', x), x', Cons(x, xs), xs1, xs2) [0]
part[False][Ite](False, x', Cons(x, xs), xs1, xs2) → part(x', xs, xs1, xs2) [0]
| qs :: S:0 → Cons:Nil → Cons:Nil Cons :: S:0 → Cons:Nil → Cons:Nil app :: Cons:Nil → Cons:Nil → Cons:Nil Nil :: Cons:Nil quicksort :: Cons:Nil → Cons:Nil part :: S:0 → Cons:Nil → Cons:Nil → Cons:Nil → Cons:Nil part[Ite] :: True:False → S:0 → Cons:Nil → Cons:Nil → Cons:Nil → Cons:Nil gr :: S:0 → S:0 → True:False notEmpty :: Cons:Nil → True:False True :: True:False False :: True:False lt :: S:0 → S:0 → True:False S :: S:0 → S:0 0 :: S:0 part[False][Ite] :: True:False → S:0 → Cons:Nil → Cons:Nil → Cons:Nil → Cons:Nil |
lt(v0, v1) → null_lt [0]
gr(v0, v1) → null_gr [0]
part[Ite](v0, v1, v2, v3, v4) → null_part[Ite] [0]
part[False][Ite](v0, v1, v2, v3, v4) → null_part[False][Ite] [0]
qs(v0, v1) → null_qs [0]
quicksort(v0) → null_quicksort [0]
part(v0, v1, v2, v3) → null_part [0]
app(v0, v1) → null_app [0]
notEmpty(v0) → null_notEmpty [0]
null_lt, null_gr, null_part[Ite], null_part[False][Ite], null_qs, null_quicksort, null_part, null_app, null_notEmpty
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Nil => 0
True => 2
False => 1
0 => 0
null_lt => 0
null_gr => 0
null_part[Ite] => 0
null_part[False][Ite] => 0
null_qs => 0
null_quicksort => 0
null_part => 0
null_app => 0
null_notEmpty => 0
app(z, z') -{ 1 }→ ys :|: z' = ys, ys >= 0, z = 0
app(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
app(z, z') -{ 1 }→ 1 + x + app(xs, ys) :|: z = 1 + x + xs, xs >= 0, z' = ys, ys >= 0, x >= 0
gr(z, z') -{ 0 }→ gr(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
gr(z, z') -{ 0 }→ 2 :|: x >= 0, z = 1 + x, z' = 0
gr(z, z') -{ 0 }→ 1 :|: y >= 0, z = 0, z' = y
gr(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
lt(z, z') -{ 0 }→ lt(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
lt(z, z') -{ 0 }→ 2 :|: z' = 1 + y, y >= 0, z = 0
lt(z, z') -{ 0 }→ 1 :|: x >= 0, z = x, z' = 0
lt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
notEmpty(z) -{ 1 }→ 2 :|: z = 1 + x + xs, xs >= 0, x >= 0
notEmpty(z) -{ 1 }→ 1 :|: z = 0
notEmpty(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
part(z, z', z'', z1) -{ 1 }→ part[Ite](gr(x', x), x', 1 + x + xs, xs1, xs2) :|: xs >= 0, xs2 >= 0, z' = 1 + x + xs, z1 = xs2, x' >= 0, x >= 0, z'' = xs1, xs1 >= 0, z = x'
part(z, z', z'', z1) -{ 1 }→ app(xs1, xs2) :|: xs2 >= 0, z1 = xs2, x >= 0, z'' = xs1, xs1 >= 0, z = x, z' = 0
part(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
part[False][Ite](z, z', z'', z1, z2) -{ 0 }→ part(x', xs, xs1, xs2) :|: z' = x', xs >= 0, xs2 >= 0, z = 1, z2 = xs2, x' >= 0, x >= 0, z1 = xs1, xs1 >= 0, z'' = 1 + x + xs
part[False][Ite](z, z', z'', z1, z2) -{ 0 }→ part(x', xs, xs1, 1 + x + xs2) :|: z = 2, z' = x', xs >= 0, xs2 >= 0, z2 = xs2, x' >= 0, x >= 0, z1 = xs1, xs1 >= 0, z'' = 1 + x + xs
part[False][Ite](z, z', z'', z1, z2) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z2 = v4, v2 >= 0, v3 >= 0
part[Ite](z, z', z'', z1, z2) -{ 0 }→ part[False][Ite](lt(x', x), x', 1 + x + xs, xs1, xs2) :|: z' = x', xs >= 0, xs2 >= 0, z = 1, z2 = xs2, x' >= 0, x >= 0, z1 = xs1, xs1 >= 0, z'' = 1 + x + xs
part[Ite](z, z', z'', z1, z2) -{ 0 }→ part(x', xs, 1 + x + xs1, xs2) :|: z = 2, z' = x', xs >= 0, xs2 >= 0, z2 = xs2, x' >= 0, x >= 0, z1 = xs1, xs1 >= 0, z'' = 1 + x + xs
part[Ite](z, z', z'', z1, z2) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z2 = v4, v2 >= 0, v3 >= 0
qs(z, z') -{ 1 }→ app(1 + x + 0, 1 + x' + quicksort(xs)) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, x >= 0, z = x'
qs(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
quicksort(z) -{ 1 }→ qs(x, part(x, 1 + x' + xs, 0, 0)) :|: xs >= 0, x >= 0, x' >= 0, z = 1 + x + (1 + x' + xs)
quicksort(z) -{ 1 }→ 0 :|: z = 0
quicksort(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
quicksort(z) -{ 1 }→ 1 + x + 0 :|: x >= 0, z = 1 + x + 0
| eq(start(V, V1, V9, V10, V33),0,[qs(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V33),0,[quicksort(V, Out)],[V >= 0]). eq(start(V, V1, V9, V10, V33),0,[part(V, V1, V9, V10, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V1, V9, V10, V33),0,[app(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V33),0,[notEmpty(V, Out)],[V >= 0]). eq(start(V, V1, V9, V10, V33),0,[lt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V33),0,[gr(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V33),0,[fun(V, V1, V9, V10, V33, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0,V33 >= 0]). eq(start(V, V1, V9, V10, V33),0,[fun1(V, V1, V9, V10, V33, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0,V33 >= 0]). eq(qs(V, V1, Out),1,[quicksort(V4, Ret11),app(1 + V2 + 0, 1 + V3 + Ret11, Ret)],[Out = Ret,V4 >= 0,V1 = 1 + V2 + V4,V3 >= 0,V2 >= 0,V = V3]). eq(quicksort(V, Out),1,[part(V5, 1 + V6 + V7, 0, 0, Ret1),qs(V5, Ret1, Ret2)],[Out = Ret2,V7 >= 0,V5 >= 0,V6 >= 0,V = 2 + V5 + V6 + V7]). eq(quicksort(V, Out),1,[],[Out = 1 + V8,V8 >= 0,V = 1 + V8]). eq(quicksort(V, Out),1,[],[Out = 0,V = 0]). eq(part(V, V1, V9, V10, Out),1,[gr(V11, V12, Ret0),fun(Ret0, V11, 1 + V12 + V13, V14, V15, Ret3)],[Out = Ret3,V13 >= 0,V15 >= 0,V1 = 1 + V12 + V13,V10 = V15,V11 >= 0,V12 >= 0,V9 = V14,V14 >= 0,V = V11]). eq(part(V, V1, V9, V10, Out),1,[app(V16, V17, Ret4)],[Out = Ret4,V17 >= 0,V10 = V17,V18 >= 0,V9 = V16,V16 >= 0,V = V18,V1 = 0]). eq(app(V, V1, Out),1,[app(V20, V21, Ret12)],[Out = 1 + Ret12 + V19,V = 1 + V19 + V20,V20 >= 0,V1 = V21,V21 >= 0,V19 >= 0]). eq(app(V, V1, Out),1,[],[Out = V22,V1 = V22,V22 >= 0,V = 0]). eq(notEmpty(V, Out),1,[],[Out = 2,V = 1 + V23 + V24,V24 >= 0,V23 >= 0]). eq(notEmpty(V, Out),1,[],[Out = 1,V = 0]). eq(lt(V, V1, Out),0,[lt(V25, V26, Ret5)],[Out = Ret5,V1 = 1 + V26,V25 >= 0,V26 >= 0,V = 1 + V25]). eq(lt(V, V1, Out),0,[],[Out = 2,V1 = 1 + V27,V27 >= 0,V = 0]). eq(lt(V, V1, Out),0,[],[Out = 1,V28 >= 0,V = V28,V1 = 0]). eq(gr(V, V1, Out),0,[gr(V29, V30, Ret6)],[Out = Ret6,V1 = 1 + V30,V29 >= 0,V30 >= 0,V = 1 + V29]). eq(gr(V, V1, Out),0,[],[Out = 1,V31 >= 0,V = 0,V1 = V31]). eq(gr(V, V1, Out),0,[],[Out = 2,V32 >= 0,V = 1 + V32,V1 = 0]). eq(fun(V, V1, V9, V10, V33, Out),0,[part(V34, V35, 1 + V36 + V37, V38, Ret7)],[Out = Ret7,V = 2,V1 = V34,V35 >= 0,V38 >= 0,V33 = V38,V34 >= 0,V36 >= 0,V10 = V37,V37 >= 0,V9 = 1 + V35 + V36]). eq(fun1(V, V1, V9, V10, V33, Out),0,[part(V39, V40, V41, 1 + V42 + V43, Ret8)],[Out = Ret8,V = 2,V1 = V39,V40 >= 0,V43 >= 0,V33 = V43,V39 >= 0,V42 >= 0,V10 = V41,V41 >= 0,V9 = 1 + V40 + V42]). eq(fun(V, V1, V9, V10, V33, Out),0,[lt(V44, V45, Ret01),fun1(Ret01, V44, 1 + V45 + V46, V47, V48, Ret9)],[Out = Ret9,V1 = V44,V46 >= 0,V48 >= 0,V = 1,V33 = V48,V44 >= 0,V45 >= 0,V10 = V47,V47 >= 0,V9 = 1 + V45 + V46]). eq(fun1(V, V1, V9, V10, V33, Out),0,[part(V49, V50, V51, V52, Ret10)],[Out = Ret10,V1 = V49,V50 >= 0,V52 >= 0,V = 1,V33 = V52,V49 >= 0,V53 >= 0,V10 = V51,V51 >= 0,V9 = 1 + V50 + V53]). eq(lt(V, V1, Out),0,[],[Out = 0,V54 >= 0,V55 >= 0,V = V54,V1 = V55]). eq(gr(V, V1, Out),0,[],[Out = 0,V56 >= 0,V57 >= 0,V = V56,V1 = V57]). eq(fun(V, V1, V9, V10, V33, Out),0,[],[Out = 0,V10 = V58,V59 >= 0,V60 >= 0,V9 = V61,V62 >= 0,V = V59,V1 = V62,V33 = V60,V61 >= 0,V58 >= 0]). eq(fun1(V, V1, V9, V10, V33, Out),0,[],[Out = 0,V10 = V63,V64 >= 0,V65 >= 0,V9 = V66,V67 >= 0,V = V64,V1 = V67,V33 = V65,V66 >= 0,V63 >= 0]). eq(qs(V, V1, Out),0,[],[Out = 0,V68 >= 0,V69 >= 0,V = V68,V1 = V69]). eq(quicksort(V, Out),0,[],[Out = 0,V70 >= 0,V = V70]). eq(part(V, V1, V9, V10, Out),0,[],[Out = 0,V10 = V71,V72 >= 0,V9 = V73,V74 >= 0,V = V72,V1 = V74,V73 >= 0,V71 >= 0]). eq(app(V, V1, Out),0,[],[Out = 0,V75 >= 0,V76 >= 0,V = V75,V1 = V76]). eq(notEmpty(V, Out),0,[],[Out = 0,V77 >= 0,V = V77]). input_output_vars(qs(V,V1,Out),[V,V1],[Out]). input_output_vars(quicksort(V,Out),[V],[Out]). input_output_vars(part(V,V1,V9,V10,Out),[V,V1,V9,V10],[Out]). input_output_vars(app(V,V1,Out),[V,V1],[Out]). input_output_vars(notEmpty(V,Out),[V],[Out]). input_output_vars(lt(V,V1,Out),[V,V1],[Out]). input_output_vars(gr(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,V9,V10,V33,Out),[V,V1,V9,V10,V33],[Out]). input_output_vars(fun1(V,V1,V9,V10,V33,Out),[V,V1,V9,V10,V33],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [app/3]
1. recursive : [gr/3]
2. recursive : [lt/3]
3. recursive : [fun/6,fun1/6,part/5]
4. non_recursive : [notEmpty/2]
5. recursive [non_tail] : [qs/3,quicksort/2]
6. non_recursive : [start/5]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into app/3
1. SCC is partially evaluated into gr/3
2. SCC is partially evaluated into lt/3
3. SCC is partially evaluated into part/5
4. SCC is partially evaluated into notEmpty/2
5. SCC is partially evaluated into quicksort/2
6. SCC is partially evaluated into start/5
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations app/3
* CE 23 is refined into CE [42]
* CE 22 is refined into CE [43]
* CE 21 is refined into CE [44]
### Cost equations --> "Loop" of app/3
* CEs [44] --> Loop 25
* CEs [42] --> Loop 26
* CEs [43] --> Loop 27
### Ranking functions of CR app(V,V1,Out)
* RF of phase [25]: [V]
#### Partial ranking functions of CR app(V,V1,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
### Specialization of cost equations gr/3
* CE 41 is refined into CE [45]
* CE 40 is refined into CE [46]
* CE 39 is refined into CE [47]
* CE 38 is refined into CE [48]
### Cost equations --> "Loop" of gr/3
* CEs [48] --> Loop 28
* CEs [45] --> Loop 29
* CEs [46] --> Loop 30
* CEs [47] --> Loop 31
### Ranking functions of CR gr(V,V1,Out)
* RF of phase [28]: [V,V1]
#### Partial ranking functions of CR gr(V,V1,Out)
* Partial RF of phase [28]:
- RF of loop [28:1]:
V
V1
### Specialization of cost equations lt/3
* CE 27 is refined into CE [49]
* CE 26 is refined into CE [50]
* CE 25 is refined into CE [51]
* CE 24 is refined into CE [52]
### Cost equations --> "Loop" of lt/3
* CEs [52] --> Loop 32
* CEs [49] --> Loop 33
* CEs [50] --> Loop 34
* CEs [51] --> Loop 35
### Ranking functions of CR lt(V,V1,Out)
* RF of phase [32]: [V,V1]
#### Partial ranking functions of CR lt(V,V1,Out)
* Partial RF of phase [32]:
- RF of loop [32:1]:
V
V1
### Specialization of cost equations part/5
* CE 28 is refined into CE [53,54,55,56,57,58,59]
* CE 31 is refined into CE [60,61,62,63,64]
* CE 34 is refined into CE [65]
* CE 33 is refined into CE [66,67,68,69]
* CE 32 is refined into CE [70,71]
* CE 30 is refined into CE [72,73]
* CE 29 is refined into CE [74,75,76]
### Cost equations --> "Loop" of part/5
* CEs [70,71] --> Loop 36
* CEs [73] --> Loop 37
* CEs [75,76] --> Loop 38
* CEs [72] --> Loop 39
* CEs [74] --> Loop 40
* CEs [69] --> Loop 41
* CEs [68] --> Loop 42
* CEs [67] --> Loop 43
* CEs [66] --> Loop 44
* CEs [53,54,55,56,57,58,59,60,61,62,63,64,65] --> Loop 45
### Ranking functions of CR part(V,V1,V9,V10,Out)
* RF of phase [36,37,38]: [V1]
* RF of phase [39,40]: [V1]
#### Partial ranking functions of CR part(V,V1,V9,V10,Out)
* Partial RF of phase [36,37,38]:
- RF of loop [36:1]:
V1
- RF of loop [37:1]:
-V+V1-1
V1-2
- RF of loop [38:1]:
-V+V1
V1-1
* Partial RF of phase [39,40]:
- RF of loop [39:1]:
V1-1
- RF of loop [40:1]:
V1
### Specialization of cost equations notEmpty/2
* CE 35 is refined into CE [77]
* CE 37 is refined into CE [78]
* CE 36 is refined into CE [79]
### Cost equations --> "Loop" of notEmpty/2
* CEs [77] --> Loop 46
* CEs [78] --> Loop 47
* CEs [79] --> Loop 48
### Ranking functions of CR notEmpty(V,Out)
#### Partial ranking functions of CR notEmpty(V,Out)
### Specialization of cost equations quicksort/2
* CE 18 is refined into CE [80]
* CE 16 is refined into CE [81,82,83,84,85]
* CE 19 is refined into CE [86]
* CE 20 is refined into CE [87]
* CE 17 is refined into CE [88,89,90,91,92,93,94,95,96,97,98,99]
### Cost equations --> "Loop" of quicksort/2
* CEs [89] --> Loop 49
* CEs [93,96,99] --> Loop 50
* CEs [92,95,98] --> Loop 51
* CEs [90] --> Loop 52
* CEs [91,94,97] --> Loop 53
* CEs [88] --> Loop 54
* CEs [80] --> Loop 55
* CEs [81,82,83,84,85,86,87] --> Loop 56
### Ranking functions of CR quicksort(V,Out)
* RF of phase [49,50,51,52,53,54]: [V/2-1/2]
#### Partial ranking functions of CR quicksort(V,Out)
* Partial RF of phase [49,50,51,52,53,54]:
- RF of loop [49:1,52:1,54:1]:
V/2-1/2
- RF of loop [50:1,51:1,53:1]:
V-2
### Specialization of cost equations start/5
* CE 8 is refined into CE [100,101,102,103,104,105,106,107,108,109,110]
* CE 9 is refined into CE [111,112,113,114,115,116,117,118]
* CE 2 is refined into CE [119]
* CE 3 is refined into CE [120,121,122,123,124,125,126,127,128]
* CE 4 is refined into CE [129,130,131,132,133]
* CE 5 is refined into CE [134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152]
* CE 6 is refined into CE [153,154,155,156,157,158,159,160,161,162,163]
* CE 7 is refined into CE [164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179]
* CE 10 is refined into CE [180,181,182]
* CE 11 is refined into CE [183,184,185,186,187,188,189,190,191,192,193]
* CE 12 is refined into CE [194,195,196,197]
* CE 13 is refined into CE [198,199,200]
* CE 14 is refined into CE [201,202,203,204,205]
* CE 15 is refined into CE [206,207,208,209,210]
### Cost equations --> "Loop" of start/5
* CEs [191] --> Loop 57
* CEs [187,188,189,190,202,207] --> Loop 58
* CEs [104,108] --> Loop 59
* CEs [100,101,102,103,105,106,107,109,110,111,112,113,114,115,116,117,118] --> Loop 60
* CEs [138,142,146,150,157,161,173,177] --> Loop 61
* CEs [129,130,131,132,133,134,135,136,137,139,140,141,143,144,145,147,148,149,151,152,153,154,155,156,158,159,160,162,163,164,165,166,167,168,169,170,171,172,174,175,176,178,179] --> Loop 62
* CEs [119,120,121,122,123,124,125,126,127,128,180,181,182,183,184,185,186,192,193,194,195,196,197,198,199,200,201,203,204,205,206,208,209,210] --> Loop 63
### Ranking functions of CR start(V,V1,V9,V10,V33)
#### Partial ranking functions of CR start(V,V1,V9,V10,V33)
Computing Bounds
=====================================
#### Cost of chains of app(V,V1,Out):
* Chain [[25],27]: 1*it(25)+1
Such that:it(25) =< -V1+Out
with precondition: [V+V1=Out,V>=1,V1>=0]
* Chain [[25],26]: 1*it(25)+0
Such that:it(25) =< Out
with precondition: [V1>=0,Out>=1,V>=Out]
* Chain [27]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [26]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of gr(V,V1,Out):
* Chain [[28],31]: 0
with precondition: [Out=1,V>=1,V1>=V]
* Chain [[28],30]: 0
with precondition: [Out=2,V1>=1,V>=V1+1]
* Chain [[28],29]: 0
with precondition: [Out=0,V>=1,V1>=1]
* Chain [31]: 0
with precondition: [V=0,Out=1,V1>=0]
* Chain [30]: 0
with precondition: [V1=0,Out=2,V>=1]
* Chain [29]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of lt(V,V1,Out):
* Chain [[32],35]: 0
with precondition: [Out=2,V>=1,V1>=V+1]
* Chain [[32],34]: 0
with precondition: [Out=1,V1>=1,V>=V1]
* Chain [[32],33]: 0
with precondition: [Out=0,V>=1,V1>=1]
* Chain [35]: 0
with precondition: [V=0,Out=2,V1>=1]
* Chain [34]: 0
with precondition: [V1=0,Out=1,V>=0]
* Chain [33]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of part(V,V1,V9,V10,Out):
* Chain [[39,40],45]: 2*it(39)+1
Such that:aux(3) =< V1
it(39) =< aux(3)
with precondition: [V=0,Out=0,V1>=1,V9>=0,V10>=0]
* Chain [[39,40],44]: 2*it(39)+2
Such that:aux(4) =< V1
it(39) =< aux(4)
with precondition: [V=0,V9=0,V10>=0,Out>=V10,V1+V10>=Out,V10+2*V1>=Out+2]
* Chain [[39,40],43]: 2*it(39)+1
Such that:aux(5) =< V1
it(39) =< aux(5)
with precondition: [V=0,Out=0,V1>=1,V9>=0,V10>=0]
* Chain [[39,40],42]: 2*it(39)+1*s(1)+2
Such that:s(1) =< V9
aux(6) =< V1
it(39) =< aux(6)
with precondition: [V=0,V9>=1,V10>=0,Out>=V9+V10,V1+V9+V10>=Out,V9+V10+2*V1>=Out+2]
* Chain [[39,40],41]: 2*it(39)+1*s(2)+1
Such that:s(2) =< V9
aux(7) =< V1
it(39) =< aux(7)
with precondition: [V=0,V1>=1,V10>=0,Out>=1,V9>=Out]
* Chain [[36,37,38],45]: 1*it(36)+2*it(37)+1
Such that:aux(8) =< -V+V1
aux(12) =< V1
it(37) =< aux(8)
it(37) =< aux(12)
it(36) =< aux(12)
with precondition: [Out=0,V>=1,V1>=1,V9>=0,V10>=0]
* Chain [[36,37,38],44]: 1*it(36)+2*it(37)+2
Such that:aux(8) =< -V+V1
aux(13) =< V1
it(37) =< aux(8)
it(37) =< aux(13)
it(36) =< aux(13)
with precondition: [V9=0,V>=1,V10>=0,V1>=V+1,Out>=V10,V1+V10>=Out,V10+3*V1>=2*V+Out+4]
* Chain [[36,37,38],43]: 1*it(36)+2*it(37)+1
Such that:aux(8) =< -V+V1
aux(14) =< V1
it(37) =< aux(8)
it(37) =< aux(14)
it(36) =< aux(14)
with precondition: [Out=0,V>=1,V1>=1,V9>=0,V10>=0]
* Chain [[36,37,38],42]: 1*it(36)+2*it(37)+1*s(1)+2
Such that:aux(8) =< -V+V1
s(1) =< -V10+Out
aux(15) =< V1
it(37) =< aux(8)
it(37) =< aux(15)
it(36) =< aux(15)
with precondition: [V>=1,V9>=0,V10>=0,Out>=V10+1,Out>=V9+V10,Out+V1>=V9+V10+2,V1+V9+V10>=Out]
* Chain [[36,37,38],41]: 1*it(36)+2*it(37)+1*s(2)+1
Such that:aux(8) =< -V+V1
s(2) =< V1+V9
aux(16) =< V1
it(37) =< aux(8)
it(37) =< aux(16)
it(36) =< aux(16)
with precondition: [V>=1,V1>=1,V9>=0,V10>=0,Out>=1,V1+V9>=Out]
* Chain [45]: 1
with precondition: [Out=0,V>=0,V1>=0,V9>=0,V10>=0]
* Chain [44]: 2
with precondition: [V1=0,V9=0,V10=Out,V>=0,V10>=0]
* Chain [43]: 1
with precondition: [V1=0,Out=0,V>=0,V9>=0,V10>=0]
* Chain [42]: 1*s(1)+2
Such that:s(1) =< V9
with precondition: [V1=0,V9+V10=Out,V>=0,V9>=1,V10>=0]
* Chain [41]: 1*s(2)+1
Such that:s(2) =< V9
with precondition: [V1=0,V>=0,V10>=0,Out>=1,V9>=Out]
#### Cost of chains of notEmpty(V,Out):
* Chain [48]: 1
with precondition: [V=0,Out=1]
* Chain [47]: 0
with precondition: [Out=0,V>=0]
* Chain [46]: 1
with precondition: [Out=2,V>=1]
#### Cost of chains of quicksort(V,Out):
* Chain [[49,50,51,52,53,54],56]: 26*it(49)+31*s(16)+2*s(109)+37*s(112)+3
Such that:aux(46) =< V/2
aux(48) =< V
s(16) =< aux(48)
it(49) =< aux(48)
it(49) =< aux(46)
aux(39) =< aux(48)
s(111) =< it(49)*aux(48)
s(114) =< it(49)*aux(39)
s(112) =< s(114)
s(109) =< s(111)
with precondition: [Out>=0,2*V>=5,V>=Out,2*V>=Out+3]
* Chain [[49,50,51,52,53,54],55]: 5*it(49)+21*it(50)+2*s(109)+8*s(110)+37*s(112)+1
Such that:aux(49) =< V
aux(50) =< V/2
it(50) =< aux(49)
s(110) =< aux(49)
it(49) =< aux(50)
it(50) =< aux(50)
aux(39) =< aux(49)
s(111) =< it(49)*aux(49)
s(114) =< it(50)*aux(39)
s(112) =< s(114)
s(109) =< s(111)
with precondition: [V>=3,Out>=0,V>=Out]
* Chain [56]: 23*s(16)+3
Such that:aux(23) =< V
s(16) =< aux(23)
with precondition: [Out=0,V>=0]
* Chain [55]: 1
with precondition: [V=Out,V>=1]
#### Cost of chains of start(V,V1,V9,V10,V33):
* Chain [63]: 310*s(147)+47*s(158)+5*s(160)+74*s(164)+2*s(165)+2*s(167)+148*s(176)+8*s(177)+64*s(195)+47*s(198)+5*s(200)+74*s(204)+2*s(205)+2*s(207)+8*s(212)+2*s(214)+2*s(221)+5
Such that:s(197) =< V/2
s(157) =< V1/2
aux(57) =< -V+V1
aux(58) =< V
aux(59) =< V1
aux(60) =< V1+V9
aux(61) =< V9
s(195) =< aux(58)
s(147) =< aux(59)
s(221) =< aux(60)
s(214) =< aux(61)
s(212) =< aux(57)
s(212) =< aux(59)
s(198) =< aux(58)
s(200) =< s(197)
s(198) =< s(197)
s(201) =< aux(58)
s(202) =< s(200)*aux(58)
s(203) =< s(198)*s(201)
s(204) =< s(203)
s(205) =< s(202)
s(206) =< s(198)*aux(58)
s(207) =< s(206)
s(161) =< aux(59)
s(174) =< s(147)*aux(59)
s(175) =< s(147)*s(161)
s(176) =< s(175)
s(177) =< s(174)
s(158) =< aux(59)
s(160) =< s(157)
s(158) =< s(157)
s(162) =< s(160)*aux(59)
s(163) =< s(158)*s(161)
s(164) =< s(163)
s(165) =< s(162)
s(166) =< s(158)*aux(59)
s(167) =< s(166)
with precondition: [V>=0]
* Chain [62]: 60*s(233)+32*s(236)+16*s(238)+8*s(247)+2
Such that:aux(63) =< -V1+V9
aux(64) =< V9
aux(65) =< V9+V10
aux(66) =< V10
s(247) =< aux(65)
s(238) =< aux(66)
s(236) =< aux(63)
s(236) =< aux(64)
s(233) =< aux(64)
with precondition: [V=1,V1>=0,V9>=1,V10>=0,V33>=0]
* Chain [61]: 8*s(328)+4*s(329)+2
Such that:aux(67) =< -V1+V9
aux(68) =< V9
s(328) =< aux(67)
s(328) =< aux(68)
s(329) =< aux(68)
with precondition: [V=1,V10=0,V1>=0,V9>=1,V33>=0]
* Chain [60]: 22*s(343)+16*s(346)+4*s(348)+12*s(357)+2
Such that:aux(71) =< -V1+V9
aux(72) =< V9
aux(73) =< V9+V10
aux(74) =< V10
s(357) =< aux(73)
s(348) =< aux(74)
s(346) =< aux(71)
s(346) =< aux(72)
s(343) =< aux(72)
with precondition: [V=2,V1>=0,V9>=1,V10>=0,V33>=0]
* Chain [59]: 2*s(390)+1*s(391)+2
Such that:s(388) =< -V1+V9
s(389) =< V9
s(390) =< s(388)
s(390) =< s(389)
s(391) =< s(389)
with precondition: [V=2,V10=0,V1>=0,V9>=1,V33>=0]
* Chain [58]: 2*s(392)+2
Such that:aux(75) =< V9
s(392) =< aux(75)
with precondition: [V1=0,V>=0]
* Chain [57]: 2*s(396)+1*s(397)+2
Such that:s(394) =< -V+V1
s(395) =< V1
s(396) =< s(394)
s(396) =< s(395)
s(397) =< s(395)
with precondition: [V9=0,V>=1,V10>=0,V1>=V+1]
Closed-form bounds of start(V,V1,V9,V10,V33):
-------------------------------------
* Chain [63] with precondition: [V>=0]
- Upper bound: 111*V+5+76*V*V+V/2* (2*V)+nat(V1)*357+nat(V1)*232*nat(V1)+nat(V1)*2*nat(V1/2)+nat(V9)*2+nat(V1+V9)*2+nat(-V+V1)*8+5/2*V+nat(V1/2)*5
- Complexity: n^2
* Chain [62] with precondition: [V=1,V1>=0,V9>=1,V10>=0,V33>=0]
- Upper bound: 68*V9+24*V10+2+nat(-V1+V9)*32
- Complexity: n
* Chain [61] with precondition: [V=1,V10=0,V1>=0,V9>=1,V33>=0]
- Upper bound: 4*V9+2+nat(-V1+V9)*8
- Complexity: n
* Chain [60] with precondition: [V=2,V1>=0,V9>=1,V10>=0,V33>=0]
- Upper bound: 34*V9+16*V10+2+nat(-V1+V9)*16
- Complexity: n
* Chain [59] with precondition: [V=2,V10=0,V1>=0,V9>=1,V33>=0]
- Upper bound: V9+2+nat(-V1+V9)*2
- Complexity: n
* Chain [58] with precondition: [V1=0,V>=0]
- Upper bound: nat(V9)*2+2
- Complexity: n
* Chain [57] with precondition: [V9=0,V>=1,V10>=0,V1>=V+1]
- Upper bound: -2*V+3*V1+2
- Complexity: n
### Maximum cost of start(V,V1,V9,V10,V33): max([nat(V9)+max([nat(-V1+V9)*2,nat(V9)+max([nat(V10)*4+nat(V9)*18+nat(V9+V10)*8+nat(-V1+V9)*8+max([nat(V9+V10)*4,nat(V10)*12+nat(V9)*38+nat(-V1+V9)*16])+ (nat(-V1+V9)*8+nat(V9)*2),111*V+3+76*V*V+V/2* (2*V)+nat(V1)*357+nat(V1)*232*nat(V1)+nat(V1)*2*nat(V1/2)+nat(V1+V9)*2+nat(-V+V1)*8+5/2*V+nat(V1/2)*5])]),nat(-V+V1)*2+nat(V1)])+2
Asymptotic class: n^2
* Total analysis performed in 1678 ms.